$\forall$${\it the\_es}$:event\_system\{i:l\}. trans(es{-}E(${\it the\_es}$); $x$,$y$.es{-}locl(${\it the\_es}$; $x$; $y$))